#2987)

* feat: deleteEdges via edge-filter Finset = deleteEdges via Set (Part of #2965)

* feat: deleteEdges via edge-filter Finset = deleteEdges via Set

Add deleteEdges_filter_edgeFinset_eq: G.deleteEdges ↑(G.edgeFinset.filter p) =
G.deleteEdges {e | p e}. Since deleteEdges ignores non-edges
(deleteEdges_eq_inter_edgeSet), deleting only the edges satisfying p equals
deleting every Sym2 satisfying p.

This bridges the Finset (Sym2 V) form of the ball-boundary bond-deletion
increment correlation_sub_deleteEdges_le_derivBound (#2974, takes E₀ : Finset)
and the Set-predicate form of the component-factorization capstone (#2986),
toward the numeric per-stage exhaustion increment.

Part of #2965

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>

---------

Co-authored-by: Claude Opus 4.7 <noreply@anthropic.com>

* feat: triple-mapped S-observable = val-image observable (Part of #2965)

* feat: triple-mapped S-observable = val-image observable

Add triple_map_subtypeUnivEquiv_eq: the observable pushed through Sum.inl,
Equiv.Finset.union S Sᶜ, and Equiv.subtypeUnivEquiv equals A.map ⟨Subtype.val,_⟩
(the plain subtype inclusion image of A in V). Via Finset.map_map the three
embeddings compose to the inclusion ↥S → V.

This identifies the observable of correlation_deleteEdges_straddle_eq_inducedGraph
(#2986) with the raw V-vertex observable (e.g. {r,s} for the pair), supplying the
observable match for the numeric per-stage increment. Together with
deleteEdges_filter_edgeFinset_eq (#2987) and correlation_congr_all (#2986), the
remaining gap is only discharging the ball-boundary hypotheses for the
straddle-edge finset.

Part of #2965

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>

---------

Co-authored-by: Claude Opus 4.7 <noreply@anthropic.com>

* feat: numeric per-stage correlation increment (Part of #2965)

* feat: numeric per-stage correlation increment (Phase A)

Add correlation_pair_sub_inducedGraph_le_derivBound (new PerStageIncrement.lean):
for r,s ∈ S, r≠s, ferromagnetic, h=0, and r,s not on any cut (straddle) edge,

  correlation G p {r,s} − correlation (inducedGraph G S) p {⟨r,_⟩,⟨s,_⟩}
    ≤ derivBound G (G.edgeFinset.filter straddle) p r s.

The full-model pair correlation exceeds the isolated induced-subgraph pair
correlation by at most the ball-boundary derivBound over the cut edges.

Composes the ball-boundary bond-deletion increment
correlation_sub_deleteEdges_le_derivBound (#2974) with the component-factorization
bridge correlation_deleteEdges_straddle_eq_inducedGraph (#2986), via
deleteEdges_filter_edgeFinset_eq (#2987) + correlation_congr_all +
triple_map_subtypeUnivEquiv_eq (#2988). The straddle predicate is @[reducible]
(to match the inline straddle set of the component lemmas under unification) and
the graph/observable bridge is a separate lemma (correlation_deleteEdges_filter_pair_eq)
to keep elaboration within the heartbeat budget.

Part of #2965

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>

* docs: fix stale 'not yet formalized' notes per codex (#2989 formalizes the composition)

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>

---------

Co-authored-by: Claude Opus 4.7 <noreply@anthropic.com>